Sequent Calculus

This tutorial is presented below as Shen source, so that it may be interactively evaluated.

\* Shen Tutorial: Sequent Calculus *\


\* I. Background

Shen's sequent calculus is a Turing-complete language for logical proof and
computation. When employed in the domain of type checking, it provides extra
power and convenience compared to the underlying Horn clause logic (Prolog)
of which it is implemented.

Sequent calculus has its origins in proof theory and mathematical logic.
A computer programmer, if having no prior experience with it in
mathematics, may find it easier to ignore the formal expositions and
concentrate on how this particular variety of the notation translates into
Shen Prolog.

Basic understanding of Shen Prolog is assumed.

It may also be helpful to disregard notions of left and right rules, since
they have no relevance from an operational standpoint. *\


\* II. T*

The internal function shen.t* is the top level implementation of the type
checking algorithm. Its parameters are an expression to type check and an
assumption context. Assumptions will be discussed later - the context can be
assumed to be an empty list for now.

The expression in the first parameter has two different input formats.
The first format contains a top level type annotation and the second does not.

In the case of the first format only, the expression is expected to have all its
function applications in curried form (unless the function is flagged 'special'
- see the Shen system function 'specialise'). *\

(package null []

 (prolog?
  (shen.t* [[+ 1 2] : T] [])
  (return T)) \\ false - not curried

 (prolog?
  (shen.t* [[[+ 1] 2] : T] [])
  (return T)) \\ number

 )



\* III. Syntax

There are two different categories of expressions - those with type annotations
and those without. Each expression category has slightly different unification
and compilation semantics. *\

(package null []

 \* 1. Basic Expressions

 We begin with an example using clauses which contain no type annotations. *\

 (datatype m0-basic

            Body1;
            BodyN;
    ______________________
            Head;)


 \* The horizontal line is referred to as the inference line. It separates
 the pattern matching head of a clause from its body.

 If during the type checking process an expression matches the head of a clause,
 the rule fires. The body clauses are then tested in turn. The flow of execution
 can therefore be read bottom up.

 When type checking, all generated datatype functions are called in the reverse
 order of their definition. This effectively merges all definitions into a
 single function for type checking all expressions.

 The above (useless and non-terminating) datatype definition translates in to
 the Prolog function below. *\

 (defprolog type#m0-basic
   Head Context <-- (shen.t* Body1 Context)
                    (shen.t* BodyN Context);)


 \* The definition loops forever because the head matches everything,
 and the tests in the body indirectly trigger self recursion. *\

 (prolog? (shen.t* Head [])) \\ maximum inferences exceeded
 (preclude [m0-basic])



 \* 2. Annotated Expressions

 The second example contains type annotations.

 Note how the pattern matching and unification mode declarations are different
 in the Prolog output compared to the previous example. *\

 (datatype m1-basic

          Body : T;
    ______________________
         Head : any;)


 (defprolog type#m1-basic
   (mode [Head : (mode any +)] -) Context <-- (shen.t* [Body : T] Context);)

 (prolog? (shen.t* Head [])) \\ false, since we deleted the m0-basic rule
 (prolog? (shen.t* [Head : any] [])) \\ maximum inferences exceeded

 (preclude [m1-basic]) )



\* IV. Assumption Context

The assumption context is an arbitrary set of facts which may be used to assist
the proof. Facts may be produced and consumed in different contexts as the
proof proceeds.

A sequent clause may depend on a certain fact being in the current context
before firing, and it may also introduce new facts when proving clauses in its
body.

Assumptions are typically introduced by 'let', 'lambda', and 'define' to
describe the variables they introduce.

Syntactically, assumptions are both consumed and produced using the >> operator.
The behavior varies based on if it is used below or above the inference line.

The left side of the operator contains one or more comma separated assumptions,
while the right side is the expression that is to be proved.

Below the inference line, assumptions indicate additional facts which must
exist in a given context before the rule is allowed to fire. If a match occurs,
the fact is removed from the current context when evaluating the clauses
above the inference line.

Above the inference line, assumptions indicate additional facts which are
to be added to the current context before type checking the expression to the
right.

The flow of execution in a sequent can therefore be followed clockwise from the
bottom-right like so:

     3 >> 4
 _____________
     2 >> 1

If expression 1 is matched and expression 2 is found in the context,
then expression 2 is removed from the context.
Expression 3 is then added to the remaining context while verifying
expression 4.


The first example below shows how a second support routine is generated
to match and discard the given assumption from the context before
proceeding *\

(package null []

 (datatype a-basic

        dog, cat >> P;
    ______________________
         fact >> P;)

 (defprolog type#a-basic P Context <-- (shen.cl11910 Context Context1)
                                       (bind ContextOut Context1)
                                       (shen.t* P [dog cat | ContextOut]);)

 (defprolog shen.cl11910
   [fact | In] In <--;
   [X|XS] [X|Out] <-- (shen.cl11910 XS Out);)

 (preclude [a-basic]) )



\* V. Extra Syntax

Certain extra syntax, unrelated to sequent calculus, is allowed to appear
before the first clause in the body. 'if' and 'let' are equivalent to 'is' and
'when' in Shen Prolog. *\

(datatype extra-if-let-cut

       if (= true true)
         let Y "abc"
              !; Z;
    ______________________
             X; )

(defprolog type#extra-if-let
  X Context <-- (when (= true true))
                (is Y "abc")
                !
                (shen.t* Z Context);)


(preclude [extra-if-let-cut])


\* Note that variables assigned by let bindings do not directly unify with the
right hand side of a type annotation, due to the way 'is' works. An extra
unification step is needed. *\

(datatype unify-something

        let Y (some test)
            (Z ~ Y);
     _______________________
          (expr X) : Z;

     ______________________
            (X ~ X);)


(preclude [unify-something])


\* VI. Verified Types

As hinted before, 'define' introduces extra assumptions to the context
before type checking its body. In addition to type information, regarding
both the function itself and its parameters, it will also add so-called verified
types generated by guard conditions.

In the below function, when trying to prove:

____________
 7 : number

The assumption context will be:

1. (integer? &&X) : verified
2. &&X : number
3. verified-test : (number --> number)


The type system can therefore assume things based on the presence of run-time
checks. *\


(define verified-test
  { number --> number }
  X -> 7 where (integer? X)
  X -> 0)



\* VII. Debug

The prolog definitions shown in this document were ported from the Horn clauses
generated by Shen's internal compilation routines.

They may be traced with the following hooks: *\

(set debug.*datatype* true)

(define datatype.trace
  Msg X -> (if (value debug.*datatype*)
               (do
                 (output "~A:~%~R~%" Msg X)
                X)
               X))


(define shen.process-datatype
  D Rules -> (let Clauses  (shen.rules->horn-clauses D Rules)
                  Compiled (shen.s-prolog
                            (datatype.trace "datatype.main" Clauses))
                (shen.remember-datatype Compiled)))

(define shen.construct-search-clause
  Pred A V -> (let Clauses [(shen.construct-base-search-clause Pred A V)
                            (shen.construct-recursive-search-clause Pred A V)]

                 (shen.s-prolog
                  (datatype.trace "datatype.search" Clauses))))